es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, Q, R:({e:E| loc(e) = loc(e1)  Id }Prop).
(e:{e:E| loc(e) = loc(e1)  Id }. Dec(Q(e)))
 ([e1,e2]~([a,b].b = first e  a.Q(e) & e[a,b).R(e))+
 (
 (e1  e2  & Q(e2) & e[e1,e2].R(e)  Q(e)) 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s), P  Q, P & Q, P  Q, t  T, x,y. t(x;y), A & B, x. t(x), {T}, e[e1,e2].P(e), T, True, e[e1,e2).P(e), A, e  e' , P  Q, x(s1,s2), [e1,e2]~([a,b].p(a;b))+, [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), x:A. B(x), e2 = first e  e1.P(e), False, (e <loc e'), Trans x,y:T. E(x;y)
Lemmas	es-pplus wf, es-loc wf, es-first-since wf, Id wf, alle-between1 wf, not wf, es-le wf, alle-between2 wf, decidable wf, es-E wf, event system wf, es-pplus functionality wrt implies, l member wf, es-interval wf, es-pplus-first-since, es-pplus-alle-between2, es-le-loc, es-loc-pred, es-locl-iff, es-locl wf, member-es-interval, es-le-trans